$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $P$, $Q$:($A$$\rightarrow\mathbb{B}$), $f$:$x$:$A$ fp$\rightarrow$ $B$($x$).
\\[0ex]filter($\lambda$${\it pL}$.$Q$(1of(${\it pL}$));fpf{-}vals(${\it eq}$;$P$;$f$)) $\sim$ fpf{-}vals(${\it eq}$;$\lambda$$a$.$P$($a$) $\wedge_{2}$ $Q$($a$);$f$)